Notes (Week 8 Wednesday)

If D is the domain of discourse

then a unary relation is a subset of D         
  a binary relation is a subset of D × D

alternatively:
  a unary relation is a function D → 𝔹
  a binary relation is a function D × D → 𝔹


  A transition relation →  ⊆   S × S

  A transition function δ : S × Σ → S


  The successor states of s:

     {s' | s → s'}


 The arithmetic expressions (aka terms)
   are the things we can put on the RHS
   of assignments

     x := 3+y              3+y is a (predicate logic) term
                           over some vocabulary

 The boolean expressions (aka wffs)
  are the things we can put as guards (conditions)
  of if-then-else statements:

    if φ then ... else ...


Usually you'd write that as a BNF grammar (Backus-Naur form grammar)

  P  :=   x := t
      |   P;P
      |   if φ then P else P fi
      |   while φ do P od

 ^ this is an inductive definition of the set 𝓛 of programs
   in disguise

   each line is an inference rule that gives you a way to
   build a new piece of program text

    φ ∈ wff      P ∈ 𝓛
  _________________________
    while φ do P od  ∈ 𝓛

We've defined the syntax of a (toy) programming language.

c.f. predicate logic: we defined
  1. a syntax for predicate logic
  2. a semantics for predicate logic ⟦φ⟧m
  3. an inference system for proving properties of formulas
      (natural deduction)
  4. prove (3) sound and complete w.r.t (2)

Now we have:
  1. a syntax for 𝓛
  2. (not now) a semantics for 𝓛
  3. an inference system for proving properties of programs
       (Hoare logic)
  4. prove Hoare logic sound and complete


  // what's true here
  <my program>
  // what's true here


  // ⊤            <-- the precondition
  x := x*2
  // x is even    <-- the postcondition

This week, we'll use a different notation:

  {⊤} x := x * 2 {x is even}


  { x=0 } x := 1 { x = 1 }

In English:

  ∀s. if ⟦x=0⟧s = true, then
      ∀s'. we can reach s' from s by
           executing x:=1,
           ⟦x=1⟧s' = true


You can't just do this:

   ____________________
    {φ} x := e {φ[x:=e]}

...sorry, can't think of a good counterexample
 on the spot.



      { 5 + z is prime }  x := 5 + z { x is prime }


Intuitively:
  if I have a valid Hoare triple,
  I should be allowed to:
   - make the precondition more specific (stronger)
   - make the postcondition more vague (weaker)

 If I have the Hoare triple

    { x is odd } P {  x = 6 }

 It should follow (intuitively) that the following
 is also valid:

    { x = 9 } P { x is even }

  {y = 1}  y := 3  { y > 1 }



  { φ } while x > 0 do x := x - 1 od {φ ∧ ¬(x > 0)}

  { x = 0 }